import Mathlib.Data.Finset.Basic

namespace CNVS

universe u v w

/-- Stato CNVS astratto: elementi validi e relazione direzionale. -/
structure CNVSState (Elem : Type u) where
  E : Set Elem
  R : Elem → Elem → Prop

/--
Modulo assiomatico minimale CNVS.

Formalizza:
- Axiom I: esistenza verificata;
- Axiom II: decomposizione finita, non uniforme, type-preserving, ricostruibile;
- Axiom III: validità globale strutturale, non ridotta alla sola validità locale.
-/
structure CNVSAxioms
    (Elem : Type u)
    (TypeTag : Type v)
    (Verifier : Type w) where

  S : CNVSState Elem

  typeOf : Elem → TypeTag
  VLocal : Elem → Prop
  VGlobal : CNVSState Elem → Prop

  ConsistentR : CNVSState Elem → Prop
  Invariant : CNVSState Elem → Prop

  D : Elem → Finset Elem
  Rec : Finset Elem → Elem
  Assign : Elem → Verifier

  infoSize : Elem → Nat

  /-- Axiom I: membership requires local verification. -/
  axiom_I_verified_existence :
    ∀ s : Elem, s ∈ S.E → VLocal s

  /-- Axiom I, strong local form. -/
  axiom_I_strong_local_form :
    ∀ s : Elem, s ∈ S.E ↔ VLocal s

  /-- Axiom II-a: every admitted element has a nonempty finite decomposition. -/
  axiom_II_nonempty_decomposition :
    ∀ s : Elem, s ∈ S.E → (D s).Nonempty

  /-- Axiom II-b: type preservation across decomposition. -/
  axiom_II_type_preservation :
    ∀ s f : Elem,
      s ∈ S.E →
      f ∈ D s →
      typeOf f = typeOf s

  /-- Axiom II-c: non-uniform fragmentation. -/
  axiom_II_non_uniformity :
    ∀ s : Elem,
      s ∈ S.E →
        ∃ fa fb : Elem,
          fa ∈ D s ∧
          fb ∈ D s ∧
          infoSize fa ≠ infoSize fb

  /-- Axiom II-d: reconstruction of the decomposition returns the original element. -/
  axiom_II_reconstruction :
    ∀ s : Elem, s ∈ S.E → Rec (D s) = s

  /--
  Axiom III-a: global validity is structurally defined.

  This corresponds to:
  VGlobal(S) = LocalOK(E) ∧ Cons_R(R,E) ∧ Inv_C(S)
  -/
  axiom_III_structural_global_validity :
    VGlobal S ↔
      (∀ s : Elem, s ∈ S.E → VLocal s) ∧
      ConsistentR S ∧
      Invariant S

  /--
  Axiom III-b: global validity is not merely local validity.

  This is expressed as the existence of a state where all local checks pass,
  but global validity fails because relation/invariant structure fails.
  -/
  axiom_III_non_reducibility_witness :
    ∃ Sbad : CNVSState Elem,
      (∀ s : Elem, s ∈ Sbad.E → VLocal s) ∧
      ¬ VGlobal Sbad

end CNVS